Termination w.r.t. Q proof of TRS/Cimelse.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)

The remaining pairs can at least be oriented weakly.

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

Used ordering: Combined order from the following AFS and order.
SUM_SUB(x1, x2) = SUM_SUB(x2)
Cons_sum(x1, x2, x3) = Cons_sum(x3)
Cons_usual(x1, x2, x3) = x3

Recursive path order with status [2].
Quasi-Precedence:

Cons_sum₁ > SUM_SUB₁

Status:

Cons_sum₁: multiset
SUM_SUB₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SUM_SUB(x1, x2) = SUM_SUB(x1, x2)
Cons_usual(x1, x2, x3) = Cons_usual(x1, x2, x3)

Recursive path order with status [2].
Quasi-Precedence:

[SUM_SUB₂, Cons_{usual_3]}

Status:

Cons_usual₃: multiset
SUM_SUB₂: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
TERM_SUB(x1, x2) = x2
Term_var(x1) = Term_var
Cons_usual(x1, x2, x3) = Cons_usual(x2, x3)
Cons_sum(x1, x2, x3) = Cons_sum(x1, x2, x3)

Recursive path order with status [2].
Quasi-Precedence:

Cons_usual₂ > [Term_var, Cons_{sum_3]}

Status:

Cons_usual₂: multiset
Term_var: multiset
Cons_sum₃: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
TERM_SUB(x1, x2) = x1
Term_sub(x1, x2) = Term_sub(x1, x2)
CONCAT(x1, x2) = x1
Case(x1, x2, x3) = Case(x1, x2, x3)
FROZEN(x1, x2, x3, x4) = FROZEN(x1, x2, x3)
Sum_sub(x1, x2) = x1
Term_inl(x1) = Term_inl(x1)
Concat(x1, x2) = Concat(x1, x2)
Cons_usual(x1, x2, x3) = Cons_usual(x1, x2, x3)
Term_app(x1, x2) = Term_app(x1, x2)
Sum_constant(x1) = Sum_constant
Right = Right
Term_pair(x1, x2) = Term_pair(x1, x2)
Term_inr(x1) = Term_inr(x1)
Left = Left
Sum_term_var(x1) = x1
Cons_sum(x1, x2, x3) = Cons_sum(x3)
Frozen(x1, x2, x3, x4) = Frozen(x3)
Id = Id
Term_var(x1) = Term_var

Recursive path order with status [2].
Quasi-Precedence:

Term_inl₁ > [Term_sub₂, Right] > Term_app₂ > [Sum_constant, Term_{pair_2]}
Term_inl₁ > [Term_sub₂, Right] > Term_inr₁ > [Sum_constant, Term_{pair_2]}
Cons_usual₃ > [Concat₂, Cons_{sum_1]} > [Term_sub₂, Right] > Term_app₂ > [Sum_constant, Term_{pair_2]}
Cons_usual₃ > [Concat₂, Cons_{sum_1]} > [Term_sub₂, Right] > Term_inr₁ > [Sum_constant, Term_{pair_2]}
Left > [Term_sub₂, Right] > Term_app₂ > [Sum_constant, Term_{pair_2]}
Left > [Term_sub₂, Right] > Term_inr₁ > [Sum_constant, Term_{pair_2]}
Frozen₁ > [Term_sub₂, Right] > Term_app₂ > [Sum_constant, Term_{pair_2]}
Frozen₁ > [Term_sub₂, Right] > Term_inr₁ > [Sum_constant, Term_{pair_2]}
Frozen₁ > Case₃ > FROZEN₃ > [Sum_constant, Term_{pair_2]}
Id > [Sum_constant, Term_{pair_2]}
Term_var > [Term_sub₂, Right] > Term_app₂ > [Sum_constant, Term_{pair_2]}
Term_var > [Term_sub₂, Right] > Term_inr₁ > [Sum_constant, Term_{pair_2]}

Status:

Term_inr₁: multiset
Term_app₂: multiset
Sum_constant: []
Term_var: multiset
Right: multiset
Case₃: [3,2,1]
Concat₂: multiset
FROZEN₃: [3,2,1]
Id: multiset
Cons_sum₁: multiset
Term_pair₂: multiset
Cons_usual₃: multiset
Term_inl₁: multiset
Left: multiset
Frozen₁: multiset
Term_sub₂: multiset

The following usable rules [14] were oriented:

Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.